Nuprl Lemma : choicef_lemma
2,24
postcript
pdf
%xm
:XM,
T
:Type,
P
:(
T
Prop). (
a
:
T
.
P
(
a
))
P
(
x
:
T
.
P
(
x
))
latex
origin
%xm:XM, T:Type, P:(T
Prop). (
a:T. P(a)) 
P(
x:T. P(x)) %xm:XM, T:Type, P:(TProp). (a:T. P(a)) P(x:T. P(x))